#include "ast_visitor.hpp"
#include "antlr_wrapper.hpp"

/* Empty by default; don't do anything upon visit */
void ASTvisitor::visit(constant *n)		{}
void ASTvisitor::visit(variable *n)		{}
void ASTvisitor::visit(array_element *n){VISIT(n->index);}
void ASTvisitor::visit(anegation *n)	{VISIT(n->arg);}
void ASTvisitor::visit(aplus *n)		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(aminus *n)		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(amultiply *n)	{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(adivide *n)		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_true *n)		{}
void ASTvisitor::visit(b_false *n)		{}
void ASTvisitor::visit(b_not *n)		{VISIT(n->arg);}
void ASTvisitor::visit(b_and *n)		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_or *n) 		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_gt *n) 		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_ge *n) 		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_lt *n) 		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_le *n) 		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_eq *n) 		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(b_neq *n) 		{VISIT(n->arg1);VISIT(n->arg2);}
void ASTvisitor::visit(sequence *n)		{for_each(n->statements, [this](statement* s){VISIT(s);});}
void ASTvisitor::visit(s_skip *n)		{}
void ASTvisitor::visit(s_read *n)		{VISIT(n->dest);}
void ASTvisitor::visit(s_write *n)		{VISIT(n->arg);}
void ASTvisitor::visit(s_if *n)			{VISIT(n->cond); VISIT(n->s_true); VISIT(n->s_false);}
void ASTvisitor::visit(s_while *n)		{VISIT(n->cond); VISIT(n->body);}
void ASTvisitor::visit(assignment *n)	{VISIT(n->dest); VISIT(n->rhs);}
void ASTvisitor::visit(program *n)		{VISIT(n->body);}

//////////////////////////////////////////////////////////////////////////////

ASTvisitorDOT::ASTvisitorDOT()
{
	this->graf = new dot;
}

ASTvisitorDOT::~ASTvisitorDOT()
{
	delete graf;
}

void ASTvisitorDOT::writeDOTfile(const char *fPath) {
	return graf->writeDOTfile(fPath);
}

void ASTvisitorDOT::StartVisit(ASTnode *n) {
	VISIT(n);			// Besøg n og alle dens børn
}
void ASTvisitorDOT::visit(constant *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", n->literal);
}
void ASTvisitorDOT::visit(variable *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", n->name);
}
void ASTvisitorDOT::visit(array_element *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", n->name + "[]");
	graf->addKant(n, n->index).Set("label", "index");
	VISIT(n->index);
}
void ASTvisitorDOT::visit(anegation *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "-");
	graf->addKant(n, n->arg);
	VISIT(n->arg);
}
void ASTvisitorDOT::visit(aplus *n)		{graf->addNode(n).Set("label", "+"); handle_children(n);}
void ASTvisitorDOT::visit(aminus *n)	{graf->addNode(n).Set("label", "-"); handle_children(n);}
void ASTvisitorDOT::visit(amultiply *n)	{graf->addNode(n).Set("label", "*"); handle_children(n);}
void ASTvisitorDOT::visit(adivide *n)	{graf->addNode(n).Set("label", "/"); handle_children(n);}
void ASTvisitorDOT::visit(b_true *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "true");
}
void ASTvisitorDOT::visit(b_false *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "false");
}
void ASTvisitorDOT::visit(b_not *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "!");
	graf->addKant(n, n->arg);
	VISIT(n->arg);
}
void ASTvisitorDOT::visit(b_and *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "&");
	graf->addKant(n, n->arg1);
	graf->addKant(n, n->arg2);
	VISIT(n->arg1);
	VISIT(n->arg2);
}
void ASTvisitorDOT::visit(b_or *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "|");
	graf->addKant(n, n->arg1);
	graf->addKant(n, n->arg2);
	VISIT(n->arg1);
	VISIT(n->arg2);
}
void ASTvisitorDOT::visit(b_gt *n) {graf->addNode(n).Set("label", ">"); handle_children(n);}
void ASTvisitorDOT::visit(b_ge *n) {graf->addNode(n).Set("label", ">="); handle_children(n);}
void ASTvisitorDOT::visit(b_lt *n) {graf->addNode(n).Set("label", "<"); handle_children(n);}
void ASTvisitorDOT::visit(b_le *n) {graf->addNode(n).Set("label", "<="); handle_children(n);}
void ASTvisitorDOT::visit(b_eq *n) {graf->addNode(n).Set("label", "="); handle_children(n);}
void ASTvisitorDOT::visit(b_neq *n) {graf->addNode(n).Set("label", "!="); handle_children(n);}
void ASTvisitorDOT::visit(assignment *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", ":=");
	graf->addKant(n, n->dest);
	graf->addKant(n, n->rhs);
	VISIT(n->dest);
	VISIT(n->rhs);
}
void ASTvisitorDOT::visit(s_skip *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "skip");
}
void ASTvisitorDOT::visit(s_read *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "read");
	graf->addKant(n, n->dest);
	VISIT(n->dest);	
}	
void ASTvisitorDOT::visit(s_write *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "write");
	graf->addKant(n, n->arg);
	VISIT(n->arg);	
}	
void ASTvisitorDOT::visit(s_if *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "if");
	graf->addKant(n, n->cond).Set("label", "cond");
	if (n->s_true)	graf->addKant(n, n->s_true).Set("label", "true");
	if (n->s_false)	graf->addKant(n, n->s_false).Set("label", "false");
	VISIT(n->cond);
	VISIT(n->s_true);
	VISIT(n->s_false);
}
void ASTvisitorDOT::visit(s_while *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "while");
	graf->addKant(n,n->cond).Set("label", "cond");
	graf->addKant(n,n->body).Set("label", "body");
	VISIT(n->cond);
	VISIT(n->body);
}
void ASTvisitorDOT::visit(sequence *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addNode(n).Set("label", "sequence");
	int cnt = 0;
	for (vector<statement*>::iterator it = n->statements.begin(); it != n->statements.end(); ++it) {
		statement *s = *it;
		graf->addKant(n, s).Set("label", cnt++);
		VISIT(s);
	}
}
void ASTvisitorDOT::visit(program *n) {
	assert(n->parent == NULL && "Parent should be NULL for program-objects");
	graf->addNode(n).Set("label", "program");
	graf->addKant(n, n->body);
	VISIT(n->body);
}

inline void ASTvisitorDOT::handle_children(b_relational *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addKant(n, n->arg1);
	graf->addKant(n, n->arg2);
	VISIT(n->arg1);
	VISIT(n->arg2);
}
inline void ASTvisitorDOT::handle_children(binary_operator *n) {
	assert(n->parent && "Parent should be set for all but program-objects");
	graf->addKant(n, n->arg1);
	graf->addKant(n, n->arg2);
	VISIT(n->arg1);
	VISIT(n->arg2);
}

////////////////////////////////////////////////////////////////////////////////

string ASTvisitorString::convert(ASTnode *n) {
	this->result = ""; 
	this->StartVisit(n); 
	this->remove_outer_parens(this->result);
	return this->result;
}
void ASTvisitorString::StartVisit(ASTnode *n)	{VISIT(n);}
void ASTvisitorString::visit(constant *n)		{result += ::stringify(n->literal);}
void ASTvisitorString::visit(variable *n)		{result += n->name;}
void ASTvisitorString::visit(array_element *n) {
	ASTvisitorString str;
	result += n->name;
	result += "[";
	result += str.convert(n->index);
	result += "]";
}
void ASTvisitorString::visit(anegation *n)	{result += "(-"; VISIT(n->arg); result += ")";}
void ASTvisitorString::visit(aplus *n)		{result += "("; VISIT(n->arg1); result+="+"; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(aminus *n)		{result += "("; VISIT(n->arg1); result+="-"; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(amultiply *n)	{result += "("; VISIT(n->arg1); result+="*"; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(adivide *n)	{result += "("; VISIT(n->arg1); result+="/"; VISIT(n->arg2); result+=")"; }

void ASTvisitorString::visit(b_true *n)		{result += "true";}
void ASTvisitorString::visit(b_false *n)	{result += "false";}
void ASTvisitorString::visit(b_not *n)		{result += "(!"; VISIT(n->arg); result += ")"; }
void ASTvisitorString::visit(b_and *n)		{result += "("; VISIT(n->arg1); result+="&"; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(b_or *n) 		{result += "("; VISIT(n->arg1); result+="|"; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(b_gt *n) 		{result += "("; VISIT(n->arg1); result+=">"; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(b_ge *n) 		{result += "("; VISIT(n->arg1); result+=">="; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(b_lt *n) 		{result += "("; VISIT(n->arg1); result+="<"; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(b_le *n) 		{result += "("; VISIT(n->arg1); result+="<="; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(b_eq *n) 		{result += "("; VISIT(n->arg1); result+="="; VISIT(n->arg2); result+=")"; }
void ASTvisitorString::visit(b_neq *n) 		{result += "("; VISIT(n->arg1); result+="!="; VISIT(n->arg2); result+=")"; }

void ASTvisitorString::visit(s_skip *n) 	{result+="skip";}
void ASTvisitorString::visit(s_read *n) 	{result+="read "; VISIT(n->dest);}
void ASTvisitorString::visit(s_write *n) 	{result+="write "; VISIT(n->arg);}
void ASTvisitorString::visit(s_if *n) {
	result+="if ";
	VISIT(n->cond);
	result+=" then\n";
	VISIT(n->s_true);
	result+="\nelse\n";
	VISIT(n->s_false);
	result+="\nfi\n";
}
void ASTvisitorString::visit(s_while *n) {
	result+="while ";
	VISIT(n->cond);
	result+=" do\n";
	VISIT(n->body);
	result+="\nod\n";
}
void ASTvisitorString::visit(sequence *n) {
	for (auto it = n->statements.begin(); it != n->statements.end(); ++it) {
		VISIT(*it);
		result+=";\n";
	}
}
void ASTvisitorString::visit(assignment *n) {VISIT(n->dest); result +=":="; VISIT(n->rhs);}
void ASTvisitorString::visit(program *n) {
	result+="program\n";
	VISIT(n->body);
	result+="\nend\n";
}
void ASTvisitorString::remove_outer_parens(string& arg) {
	if (arg.empty()) return;

	const int first = 0;
	const int last = arg.size()-1;
	if (arg[first] == '(' && arg[last] == ')') {
		arg.erase(arg.begin()+last); // remove last-char first
		arg.erase(arg.begin()+first); // followed by the first-char
	}
}

////////////////////////////////////////////////////////////////////////////////

void ASTvisitorFV::StartVisit(ASTnode *n) {
	VISIT(n);
}
set<lvalue*> ASTvisitorFV::getFV() const {
	return this->fv;
}
void ASTvisitorFV::visit(variable *n) {
	this->fv.insert(n);
}
void ASTvisitorFV::visit(array_element *n) {
	this->fv.insert(n);
}

//////////////////////////////////////////////////////////////////////////////

void ASTvisitorUses::StartVisit(ASTnode *n) {
	assert(false && "Use convert() instead");
}
set<string> ASTvisitorUses::convert(ASTnode *n) {
	this->uses.clear();
	VISIT(n);
	return this->uses;
}
void ASTvisitorUses::visit(variable *n) {
	this->uses.insert(n->name);
}
void ASTvisitorUses::visit(array_element *n) {
	this->uses.insert(n->name);
	VISIT(n->index);
}
void ASTvisitorUses::visit(assignment *n) {
	/* Dont visit n->lhs since it is a definition */
	VISIT(n->rhs);
	if (TRY_TYPE(array_element*, ae, n->dest)) {
		VISIT(ae->index);
	}
}
void ASTvisitorUses::visit(s_write *n) {
	VISIT(n->arg);
}
void ASTvisitorUses::visit(s_read *n) {
	if (TRY_TYPE(array_element*, ae, n->dest)) {
		VISIT(ae->index);
	}
}

//////////////////////////////////////////////////////////////////////////////

void ASTvisitorDefs::StartVisit(ASTnode *n) {
	VISIT(n);
}
set<string> ASTvisitorDefs::getDefs() const {
	return this->defs;
}
void ASTvisitorDefs::visit(variable *n) {
	this->defs.insert(n->name);
}
void ASTvisitorDefs::visit(array_element *n) {
	this->defs.insert(n->name);
	/* We are at A[a1], here a1 is always a use so we skip it */
}
void ASTvisitorDefs::visit(assignment *n) {
	VISIT(n->dest); // visit only left-hand side
}
void ASTvisitorDefs::visit(s_read *n) {
	VISIT(n->dest);
}
void ASTvisitorDefs::visit(s_write *n) {
	/* Do nothing: a write statement has only uses */
}

//////////////////////////////////////////////////////////////////////////////

ASTvisitorCFG::head_tail ASTvisitorCFG::visit_getReturn(ASTnode *n) {
	VISIT(n);
	assert(!args.empty() && "Intet at returnere");
	head_tail ret = args.top(); args.pop();	// læs toppen, pop derefter toppen af
	return ret;	
}

void ASTvisitorCFG::Return(const head_tail& arg) {
	this->args.push(arg);
}

CFGvertex* ASTvisitorCFG::convert(ASTnode* n) {
	this->StartVisit(n);
	assert(args.size() == 1);
	return this->args.top().head;
}

void ASTvisitorCFG::StartVisit(ASTnode *n) {
	VISIT(n);
}

void ASTvisitorCFG::visit(s_skip *n) {this->handle_atomic(n);}
void ASTvisitorCFG::visit(s_read *n) {this->handle_atomic(n);}
void ASTvisitorCFG::visit(s_write *n) {this->handle_atomic(n);}
void ASTvisitorCFG::visit(assignment *n) {this->handle_atomic(n);}

void ASTvisitorCFG::visit(s_if *n) {
	diamond *diam = new diamond();
	diam->condition = n->cond;
	
#ifdef NO_PREDS	
	head_tail t = visit_getReturn(n->s_true);
	head_tail f = visit_getReturn(n->s_false);

	diam->true_branch.setDestination(t.head);
	diam->false_branch.setDestination(f.head);
	
	head_tail ret;
	ret.head = diam;
	ret.tail.insert(t.tail.begin(), t.tail.end());
	ret.tail.insert(f.tail.begin(), f.tail.end());
#else
	box* t_pred_box = new box();
	t_pred_box->payload = n->cond;
	head_tail t = visit_getReturn(n->s_true);

	box* f_pred_box = new box();
	f_pred_box->payload = new b_not(n->cond);
	head_tail f = visit_getReturn(n->s_false);

	head_tail t_pred;
	t_pred.head = t_pred_box;
	t_pred.tail = {&(t_pred_box->child)};
	head_tail f_pred;
	f_pred.head = f_pred_box;
	f_pred.tail = {&(f_pred_box->child)};

	t_pred.append(t);
	f_pred.append(f);
	
	diam->true_branch.setDestination(t_pred.head);
	diam->false_branch.setDestination(f_pred.head);
	
	head_tail ret;
	ret.head = diam;
	ret.tail.insert(t_pred.tail.begin(), t_pred.tail.end());
	ret.tail.insert(f_pred.tail.begin(), f_pred.tail.end());	
#endif

	Return(ret);
}

void ASTvisitorCFG::visit(s_while *n) {
	diamond *diam = new diamond();
	diam->condition = n->cond;
	
#ifdef NO_PREDS
	head_tail body = visit_getReturn(n->body);

	// then-branch points to head of body
	diam->true_branch.setDestination(body.head);
	
	// let tails of body point to diamond
	for (set<CFGedge*>::iterator it = body.tail.begin(); it != body.tail.end(); ++it) {
		CFGedge *body_tail = *it;
		
		body_tail->setDestination(diam);
	}
	
	head_tail ret;
	ret.head = diam;
	ret.tail.insert(&(diam->false_branch));

#else
	box* t_pred_box = new box();
	t_pred_box->payload = n->cond;
	
	head_tail body = visit_getReturn(n->body);

	box* f_pred_box = new box();
	f_pred_box->payload = new b_not(n->cond);


	head_tail t_pred;
	t_pred.head = t_pred_box;
	t_pred.tail = {&(t_pred_box->child)};
	head_tail f_pred;
	f_pred.head = f_pred_box;
	f_pred.tail = {&(f_pred_box->child)};

	t_pred.append(body);
//	f_pred.append(f); we have nothing to append to f_pred

	diam->true_branch.setDestination(t_pred.head);
	diam->false_branch.setDestination(f_pred.head);

	for (set<CFGedge*>::iterator it = t_pred.tail.begin(); it != t_pred.tail.end(); ++it) {
		CFGedge *body_tail = *it;
		
		body_tail->setDestination(diam);
	}

	head_tail ret;
	ret.head = diam;
	ret.tail.insert(f_pred.tail.begin(), f_pred.tail.end());
#endif
	
	Return(ret);
}

void ASTvisitorCFG::visit(sequence *n) {
	head_tail ret;

	assert(!n->statements.empty());
	ret = visit_getReturn(n->statements[0]);

	for (int i = 1 /*skip nr 0*/; i < n->statements.size(); i++) {
		ret.append( visit_getReturn(n->statements[i]) );
	}

	Return(ret);
}

void ASTvisitorCFG::visit(program *n) {
	Return(visit_getReturn(n->body));
}

void ASTvisitorCFG::handle_atomic(atomic_statement *n) {
	box *ny = new box();
	ny->payload = n;
	
	head_tail ret;
	ret.head = ny;
	ret.tail.insert(&(ny->child));
	
	Return(ret);
}

void ASTvisitorCFG::head_tail::append(const head_tail& addenum) {
	assert(addenum.head);
	assert(addenum.tail.size() >= 1);
	
	// All outgoing edges from the current tails should point at addenum's head
	for (set<CFGedge*>::iterator it = this->tail.begin(); it != this->tail.end(); ++it) {
		CFGedge *curr_tail = *it;
		
		curr_tail->setDestination(addenum.head);
	}

	// Addenum has been inserted above, so addenums tail is the new overall tail
	this->tail = addenum.tail;
	assert(this->tail.size() >= 1);
}


////////////////////////////////////////////////////////////////////////////////

ASTvisitorAs::ASTvisitorAs(DS& _sigma) 
:	sigma(_sigma)
{
}

Interval ASTvisitorAs::get_interval(ASTnode *n) {
	return visit_getReturn(n);
}
void ASTvisitorAs::StartVisit(ASTnode *n) {
	assert(false && "You should use get_interval() instead");
}
void ASTvisitorAs::visit(constant *n) {
	Interval ret(n->literal, n->literal);
	Return(ret);	
}
void ASTvisitorAs::visit(variable *n) {
	Interval ret = this->lookup_in_sigma(n->name);
	Return(ret);
}
void ASTvisitorAs::visit(array_element *n) {
	Interval ret = this->lookup_in_sigma(n->name);
	Return(ret);
}
void ASTvisitorAs::visit(aplus *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 + i2;
	Return(ret);
}
void ASTvisitorAs::visit(aminus *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 - i2;
	Return(ret);
}
void ASTvisitorAs::visit(amultiply *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 * i2;
	
	if (is_algebraically_equivalent(n->arg1, n->arg2)) {
		assert((i1.lower() == i2.lower()) && (i1.upper() == i2.upper())); // intervals should span the same range
		if (i1.lower().is_negative() && i1.upper().is_positive()) {
			ret = Interval(0, std::max(i1.lower()*i1.lower(), i1.upper()*i1.upper()));
//			cout << "Converted " << i1 << "*" << i2 << " to " << ret << endl;
		}
	}
	
	Return(ret);	
}
void ASTvisitorAs::visit(adivide *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 / i2;
	
	if (is_algebraically_equivalent(n->arg1, n->arg2)) {
		assert((i1.lower() == i2.lower()) && (i1.upper() == i2.upper())); // intervals should span the same range
		const bool zero_included = (i1.lower() <= 0 && 0 <= i1.upper());
		/**
		 * If div-by-0 is not possible, then x/x == 1
         */
		if (!zero_included) { 
			ret = Interval(1,1);
//			cout << "Converted " << i1 << "/" << i2 << " to " << ret << endl;
		}
	}
	
	Return(ret);	
}
void ASTvisitorAs::visit(anegation *n) {
	Interval i1 = visit_getReturn(n->arg);
	Interval ret = -i1;
	Return(ret);
}
Interval ASTvisitorAs::visit_getReturn(ASTnode *n) {
	VISIT(n);
	assert(!args.empty() && "Intet at returnere");
	Interval ret = args.top(); args.pop();	// læs toppen, pop derefter toppen af
	return ret;
}

void ASTvisitorAs::Return(Interval ret_val) {
	this->args.push(ret_val);
}

Interval ASTvisitorAs::lookup_in_sigma(const string& var_name) {
	signs& sig = this->sigma[var_name];

	static const string P = "+";
	static const string N = "-";
	static const string Z = "0";
	static const iint inf = iint::inf();
	
	Interval ret;
	if (sig == signs({}))		{ret = Interval(0,0);}
	if (sig == signs({Z}))		{ret = Interval(0,0);}
	if (sig == signs({P}))		{ret = Interval(1,inf);}
	if (sig == signs({N}))		{ret = Interval(-inf,-1);}
	if (sig == signs({P,N}))	{ret = Interval(-inf,inf);}	// we can not handle that 0 is excluded
	if (sig == signs({Z,P}))	{ret = Interval(0,inf);}
	if (sig == signs({Z,N}))	{ret = Interval(-inf,0);}
	if (sig == signs({N,Z,P}))	{ret = Interval(-inf,inf);}

	return ret;
}

////////////////////////////////////////////////////////////////////////////////

ASTvisitorAi::ASTvisitorAi(IV& _sigma) 
:	sigma(_sigma)
{
}

Interval ASTvisitorAi::get_interval(ASTnode *n) {
	return visit_getReturn(n);
}
IV ASTvisitorAi::get_new_sigma(bexp *n) {
	return visit_getReturnIV(n);
}
void ASTvisitorAi::StartVisit(ASTnode *n) {
	VISIT(n);
}
void ASTvisitorAi::visit(b_true *n)		{ReturnIV(IV());}	// see report
void ASTvisitorAi::visit(b_false *n)	{ReturnIV(IV());}	// see report
void ASTvisitorAi::visit(b_and *n)		{ReturnIV(IV());}	// see report
void ASTvisitorAi::visit(b_or *n) 		{ReturnIV(IV());}	// see report
void ASTvisitorAi::visit(b_not *n) {
	IV intervals = visit_getReturnIV(n->arg);

	// We try to avoid ending up in the last else (whith interval_invert), as it is unprecise
	
	if (TRY_TYPE(b_ge*, op, n->arg)) {
		// We have !(x>=y) but transform to x<y
		b_lt* hack = new b_lt(op->arg1, op->arg2);
		intervals = visit_getReturnIV(hack);
	} else if (TRY_TYPE(b_gt*, op, n->arg)) {
		// We have !(x>y) but transform to x<=y
		b_le* hack = new b_le(op->arg1, op->arg2);
		intervals = visit_getReturnIV(hack);
	} else if (TRY_TYPE(b_le*, op, n->arg)) {
		// We have !(x<=y) but transform to x>y
		b_gt* hack = new b_gt(op->arg1, op->arg2);
		intervals = visit_getReturnIV(hack);
	} else if (TRY_TYPE(b_lt*, op, n->arg)) {
		// We have !(x<y) but transform to x>=y
		b_ge* hack = new b_ge(op->arg1, op->arg2);
		intervals = visit_getReturnIV(hack);
	} else if (TRY_TYPE(b_eq*, op, n->arg)) {
		// We have !(x=y) but transform to x!=y
		b_neq* hack = new b_neq(op->arg1, op->arg2);
		intervals = visit_getReturnIV(hack);
	} else if (TRY_TYPE(b_neq*, op, n->arg)) {
		// We have !(x!=y) but transform to x==y
		b_eq* hack = new b_eq(op->arg1, op->arg2);
		intervals = visit_getReturnIV(hack);
	} else {
		// Calling interval_invert is safe, but unprecise
		for_each(intervals, [&](pair<string, Interval> intr){
			intervals[intr.first] = interval_invert(intr.second);
		});
	}
	
	ReturnIV(intervals);
}
void ASTvisitorAi::visit(b_lt *n) {
	// We have x<y but transform to x<=y-1
	b_le* hack = new b_le(n->arg1, new aminus(n->arg2, new constant(1)));
	IV ret = visit_getReturnIV(hack);
	ReturnIV(ret);	
}
void ASTvisitorAi::visit(b_gt *n) {
	// We have a>b, but transform to a-1>=b
	b_ge* hack = new b_ge(new aminus(n->arg1, new constant(1)), n->arg2);
	IV ret = visit_getReturnIV(hack);
	ReturnIV(ret);
}
void ASTvisitorAi::visit(b_ge *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);

//	debugf(n);
//	debugf(i1);
//	debugf(i2);
	
	iint i1_better_lower = std::max(i1.lower(), i2.lower());
	iint i1_better_upper = i1.upper(); // not dependant on i2 !!
	Interval i1_better(i1_better_lower, i1_better_upper);

	iint i2_better_lower = i2.lower(); // not dependant on i1 !!
	iint i2_better_upper = std::min(i1.upper(), i2.upper());
	Interval i2_better(i2_better_lower, i2_better_upper);
	
	IV new_sigma = awesome(i1_better, i2_better, n->arg1, n->arg2);
	
	ReturnIV(new_sigma);
}
void ASTvisitorAi::visit(b_le *n) {
	// We have x<=y but transform to y>=x
	b_ge* hack = new b_ge(n->arg2, n->arg1);
	IV ret = visit_getReturnIV(hack);
	ReturnIV(ret);		
}
void ASTvisitorAi::visit(b_eq *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval i12_better = interval_intersection(i1, i2);
	IV new_sigma = awesome(i12_better, i12_better, n->arg1, n->arg2);
	
	debugf(i1);
	debugf(i2);
	debugf(i12_better);
	debugf(new_sigma);
	
	ReturnIV(new_sigma);
}
void ASTvisitorAi::visit(b_neq *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	IV new_sigma;

	/*
	 *	Note that it is not safe to remove the common part where they are equal
	 */
	
//	debugf(i1);
//	debugf(i2);
	
	bool simple = false;
	if (boost::numeric::singleton(i1) && boost::numeric::singleton(i2)) {
		assert(i1.lower() == i1.upper());
		assert(i2.lower() == i2.upper());
		
		if (i1.lower() == i2.lower()) {
			// Intervals are a single value, and equal

			// Reset all variables to empty interval
			ASTvisitorUses u;
			auto vars = set_union(u.convert(n->arg1), u.convert(n->arg2));
			for_each(vars, [&](string var){
				new_sigma[var] = Interval::empty();
			});
			simple = true;
		}
	}
	
	if (!simple) {
		/* 
		 * We have x!=y but do not transform into !(x==y):
		 * If we do this however, an infinite recursion can arise: (!(x==y) has 
		 * NOT as root, and the b_not method will pattern match for neq, calling us again.
		 * So we do the failover rule in b_not method ourselves.
		 */
		b_eq* hack = new b_eq(n->arg1, n->arg2);
		new_sigma = visit_getReturnIV(hack);
		for_each(new_sigma, [&](pair<string, Interval> intr){
			new_sigma[intr.first] = interval_invert(intr.second);
		});
	}

	if ((!boost::numeric::empty(i1)) && (!boost::numeric::empty(i2))) {
		if (i1.upper()==iint::inf() && i2.upper()==iint::inf()) {
			new_sigma = this->sigma;
		}
	}
	
	debugf(new_sigma);
	
	ReturnIV(new_sigma);			
}
void ASTvisitorAi::visit(constant *n) {
	Interval ret(n->literal, n->literal);
	ret = prune(ret);
	Return(ret);	
}
void ASTvisitorAi::visit(variable *n) {
	Interval ret = this->lookup_in_sigma(n->name);
	ret = prune(ret);
	Return(ret);
}
void ASTvisitorAi::visit(array_element *n) {
	Interval not_used = visit_getReturn(n->index); // We don't consider elements of the array, only the entire array
	Interval ret = this->lookup_in_sigma(n->name);
	ret = prune(ret);
	Return(ret);
}
void ASTvisitorAi::visit(aplus *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 + i2;
	ret = prune(ret);
	Return(ret);
}
void ASTvisitorAi::visit(aminus *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 - i2;
	ret = prune(ret);
	Return(ret);
}
void ASTvisitorAi::visit(amultiply *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 * i2;
	
	if (is_algebraically_equivalent(n->arg1, n->arg2)) {
		assert((i1.lower() == i2.lower()) && (i1.upper() == i2.upper())); // intervals should span the same range
		if (i1.lower().is_negative() && i1.upper().is_positive()) {
			ret = Interval(0, std::max(i1.lower()*i1.lower(), i1.upper()*i1.upper()));
//			cout << "Converted " << i1 << "*" << i2 << " to " << ret << endl;
		}
	}
	
	ret = prune(ret);
	Return(ret);	
}
void ASTvisitorAi::visit(adivide *n) {
	Interval i1 = visit_getReturn(n->arg1);
	Interval i2 = visit_getReturn(n->arg2);
	Interval ret = i1 / i2;
	
	if (is_algebraically_equivalent(n->arg1, n->arg2)) {
		assert((i1.lower() == i2.lower()) && (i1.upper() == i2.upper())); // intervals should span the same range
		const bool zero_included = (i1.lower() <= 0 && 0 <= i1.upper());
		/**
		 * If div-by-0 is not possible, then x/x == 1
         */
		if (!zero_included) { 
			ret = Interval(1,1);
//			cout << "Converted " << i1 << "/" << i2 << " to " << ret << endl;
		}
	}
	
	ret = prune(ret);
	Return(ret);	
}
void ASTvisitorAi::visit(anegation *n) {
	Interval i1 = visit_getReturn(n->arg);
	Interval ret = -i1;
	ret = prune(ret);
	Return(ret);
}
Interval ASTvisitorAi::visit_getReturn(ASTnode *n) {
	VISIT(n);
	assert(!args.empty() && "Intet at returnere");
	Interval ret = args.top(); args.pop();	// læs toppen, pop derefter toppen af
	return ret;
}
void ASTvisitorAi::Return(Interval ret_val) {
	this->args.push(ret_val);
}
IV ASTvisitorAi::visit_getReturnIV(bexp *n) {
	VISIT(n);
	assert(!argsIV.empty() && "Intet at returnere");
	IV ret = argsIV.top(); argsIV.pop();	// læs toppen, pop derefter toppen af
	return ret;
}
void ASTvisitorAi::ReturnIV(IV ret_val) {
	this->argsIV.push(ret_val);
}
Interval ASTvisitorAi::lookup_in_sigma(const string& var_name) {
	Interval& inter = this->sigma[var_name];
	return inter;
}

IV ASTvisitorAi::awesome(Interval i1_better, Interval i2_better, arith* arg1, arith* arg2)
{
	debugf(i1_better);
	debugf(i2_better);
	
	// Lav projection 
	IV sigma1;
	IV sigma2;
	IV sigma3;
	IV sigma4;
	
	bool predicate_always_false = false;
	if (!boost::numeric::empty(i1_better)) {
		sigma1 = project(arg1, i1_better.lower(), this->sigma);
		sigma2 = project(arg1, i1_better.upper(), this->sigma); 
	} else {
		predicate_always_false = true;
	}
	if (!boost::numeric::empty(i2_better)) {
		sigma3 = project(arg2, i2_better.lower(), this->sigma);
		sigma4 = project(arg2, i2_better.upper(), this->sigma);
	} else {
		predicate_always_false = true;
	}

	IV new_sigma;

	if (predicate_always_false) {
		/*
		 *	This predicate is always false, so what should the interval of variables below it be?
		 *	Well, nothing - ie. bottom. We represent bottom by an empty interval.
		 */
		ASTvisitorUses u;
		auto vars = set_union(u.convert(arg1), u.convert(arg2));
		for_each(vars, [&new_sigma](string var){
			new_sigma[var] = Interval::empty();
		});
	} else {
		new_sigma = IV_union(new_sigma, sigma1);
		new_sigma = IV_union(new_sigma, sigma2);
		new_sigma = IV_union(new_sigma, sigma3);
		new_sigma = IV_union(new_sigma, sigma4);
	}

	debugf(this->sigma);
	debugf(new_sigma);
	debugf(sigma1);
	debugf(sigma2);
	debugf(sigma3);
	debugf(sigma4);	
	
	return new_sigma;
}
////////////////////////////////////////////////////////////////////////////////

hash_t ASTvisitorHash::convert(ASTnode *n) {
	this->args = std::stack<hash_t>(); // clear the stack
	return visit_getReturn(n);
}
void ASTvisitorHash::StartVisit(ASTnode *n) {
	assert(false && "Use hash() instead");
}
void ASTvisitorHash::visit(constant *n) {
	Return(n->literal);
}
void ASTvisitorHash::visit(variable *n) {
	Return(get_hash(n->name));
}
void ASTvisitorHash::visit(array_element *n) {
	hash_t h_name = get_hash(n->name);
	hash_t h_indx = visit_getReturn(n->index);
	Return(h_name ^ h_indx); // xor together
}
void ASTvisitorHash::visit(aplus *n) {
	hash_t h1 = visit_getReturn(n->arg1);
	hash_t h2 = visit_getReturn(n->arg2);
	Return(h1+h2);
}
void ASTvisitorHash::visit(aminus *n) {
	hash_t h1 = visit_getReturn(n->arg1);
	hash_t h2 = visit_getReturn(n->arg2);
	Return(h1-h2);
}
void ASTvisitorHash::visit(amultiply *n) {
	hash_t h1 = visit_getReturn(n->arg1);
	hash_t h2 = visit_getReturn(n->arg2);
	Return(h1*h2);
}
void ASTvisitorHash::visit(adivide *n) {
	hash_t h1 = visit_getReturn(n->arg1);
	hash_t h2 = visit_getReturn(n->arg2);
	Return(h1/h2);
}
void ASTvisitorHash::visit(anegation *n) {
	hash_t h1 = visit_getReturn(n->arg);
	Return(-h1);
}
hash_t ASTvisitorHash::visit_getReturn(ASTnode *n) {
	VISIT(n);
	assert(!args.empty() && "Intet at returnere");
	hash_t ret = args.top(); args.pop();	// læs toppen, pop derefter toppen af
	return ret;
}
void ASTvisitorHash::Return(hash_t ret_val) {
	this->args.push(ret_val);
}


////////////////////////////////////////////////////////////////////////////////

Interval prune(const Interval& arg) 
{
	if (boost::numeric::empty(arg)) return arg;	// can't prune something that's empty
	
	static const iint cutoff_max = iint(40);
	static const iint cutoff_min = iint(-40);

	iint upper = arg.upper();
	iint lower = arg.lower();

	if (upper > cutoff_max) 
		upper = iint::inf();
	else if (upper < cutoff_min)
		upper = cutoff_min;
	
	if (lower > cutoff_max) 
		lower = cutoff_max;
	else if (lower < cutoff_min)
		lower = -iint::inf();
	
	assert(lower <= upper);
	Interval ret(lower, upper);
	return ret;
}

void prune_test() {
	debugf(prune(Interval::empty()));
	debugf(prune(Interval(-10,0)));
	debugf(prune(Interval(-10,-2)));
	debugf(prune(Interval(2,3)));
	debugf(prune(Interval(-2,3)));
	debugf(prune(Interval(-20000,3)));
	debugf(prune(Interval(-20000,30000)));
	debugf(prune(Interval(+20000,30000)));
	debugf(prune(Interval(-123456,-1234)));
	debugf(prune(Interval(+20000,iint::inf())));
	debugf(prune(Interval(-iint::inf(),iint::inf())));	
}

/**
 * Returns true if it can be determined if arg1 and arg2 always produce the same result; otherwise false.
 * If arguments::safe is false then we can not be 100% certain, but only 99.99999999999999999999999999999999999970612641229442812301%
 * The chance of arg1 and arg2 having the same hash is 1 out of (2^64) * (2^64).
 */
bool is_algebraically_equivalent(ASTnode *arg1, ASTnode *arg2) {
	static map<pair<ASTnode*,ASTnode*>, bool> memoized;

	auto arg12 = make_pair(arg1,arg2);
	bool already_computed = memoized.count(arg12);
	if (already_computed) {
		return memoized[arg12];
	}
	
	bool equal;
	string warning;
	if (arguments::safe) {
		ASTvisitorString str;
		equal = (str.convert(arg1) == str.convert(arg2));
	} else {
		ASTvisitorHash hsh;
		equal = (hsh.convert(arg1) == hsh.convert(arg2));
		
		ASTvisitorString str;
		bool equal_lexically = (str.convert(arg1) == str.convert(arg2));

		if (equal && !equal_lexically) // hash says they're equal, but they're not lexically equal
			warning = "This is only very likely to be true.";
	}
	
	if (equal && arguments::verbose) {
		cerr << "Detected '" <<  arg1 << "' and '" << arg2 << "' as being equal. " << warning << endl;
	}

	memoized[arg12] = equal;
	return equal;
}


/**
 * Example:	
 *	Assume we know:
 *		orig_sigma:
 *			x € [-1,4]
 *			z € [-1,1]
 *		root and target_value (where root is '(2+x)-z' and target_value is 5):
 *			(2+x)-z >= 5
 *	Ie. we know that 5 belongs to the interval of (2+x)-z.
 *	Then this function tries to be more precise about x and z, than stated in orig_sigma.
 *	In fact, with the above information, we can find that x can not be one of {-1,0,1} as that would violate that (2+x)-z >= 5.
 *	Hence this function will return a more sigma: {x->[2..4],z->[-1..1]}
 * 
 * @param root			The arithmetic expression containing the variables we want to be more precise about
 * @param target_value	We know this value belongs to the interval of the arithmetic expression
 * @param orig_sigma	Contains the intervals of the variables in the arithmetic expression
 * @return				A (possibly) more precise map of intervals of the variables.
 */
IV project(arith *root, iint target_value, IV& orig_sigma) 
{
	IV new_sigma;
	ASTvisitorUses uses;
	auto vars = uses.convert(root);
	
	for_each(vars, [&](string var)
	{
		Interval orig_interval = orig_sigma[var];
		Interval new_interval = Interval::empty();

		// We can't iterate over infinities, so check for them
		bool contains_infinities = false;
		contains_infinities |= boost::numeric::in(iint::inf(), orig_interval);
		contains_infinities |= boost::numeric::in(-iint::inf(), orig_interval);

		if (!contains_infinities) {
			for (iint i = orig_interval.lower(); i <= orig_interval.upper(); i++) 
			{
				IV sigma_substitued = orig_sigma; // make copy
				sigma_substitued[var] = Interval(i,i);

				ASTvisitorAi eval(sigma_substitued);
				Interval sub_interval = eval.get_interval(root);

				if (boost::numeric::in(target_value, sub_interval)) {
					new_interval = interval_union(new_interval, Interval(i,i));
				}
			}
		} else {
			// We can't make the interval any more precise; keep it unchanged
			new_interval = orig_interval;
		}
		
		new_interval = interval_intersection(new_interval, orig_interval);
		new_sigma[var] = new_interval;
	});
	
	return new_sigma;
}

set<array_element*> ASTvisitorGetArrays::convert(ASTnode* n) {
	this->arrays.clear();
	VISIT(n);
	return this->arrays;
}
void ASTvisitorGetArrays::StartVisit(ASTnode *n) {
	assert(false && "Use convert()");
}
void ASTvisitorGetArrays::visit(array_element *n) {
	this->arrays.insert(n);
	VISIT(n->index);
}
	
void project_test() 
{
/*
 * Visualize with Mathematica:
 * RegionPlot[(3 + x) + x*z - z*z*2 >= 5, {x,-1,4}, {z,-1,5}, AxesLabel->Automatic]
 */
#define PROJ1

#ifdef PROJ1
//	arith *lhs = parse_as_arith("(2+x)-z");
	arith *lhs = parse_as_arith("(3 + x) + x*z - z*z*2");
	constant *rhs = new constant(5);
	b_ge *root = new b_ge(lhs, rhs);

	IV old_sigma = {{"x",Interval(-1,4)}, {"z",Interval(-1,5)}};				// Nice
//	IV old_sigma = {{"x",Interval(-iint::inf(),4)}, {"z",Interval(-1,1)}};
//	IV old_sigma = {{"x",Interval(-1,4)}, {"z",Interval(-1,iint::inf())}};		// Nice
//	IV old_sigma = {{"x",Interval::empty()}, {"z",Interval(-1,1)}};
	IV new_sigma = project(lhs, rhs->literal, old_sigma);
#endif

#ifdef PROJ2
	arith *lhs = parse_as_arith("x");
	constant *rhs = new constant(10);
	b_ge *root = new b_ge(lhs, rhs);

	IV old_sigma = {{"x",Interval(-10,10)}};
	IV new_sigma = project(lhs, rhs->literal, old_sigma);
#endif

	debugf(root);
	debugf(old_sigma);
	debugf(new_sigma);
}
